docs: record the Coq proof gate and the 2026-07-29 rescue session - #712
Conversation
Human-readable and machine-readable documentation of the state established this session, using the conventions already in the repo rather than new ones. - docs/ci/COQ-PROOF-GATE.adoc — sits beside required-checks.adoc. Covers what the gate checks, why it is fail-closed (and why tools/check-proofs.sh is not a model to copy), the two coqorg-under-GitHub-Actions container faults that each cost a red run, how to run it locally, and the falsifiers proving both guards can actually fail. - .machine_readable/sessions/2026-07-29-proof-gate-and-rescue.a2ml — session record on the existing a2ml/session-record/v1 schema, alongside the 2026-05-27 entry. Records the gate, the rescue of 3 feature commits from a deleted checkout, three pieces of sweep damage (including the .gitattributes deletion that would have unlabelled 493 .affine files), the partial-merge incident that left main red, and method notes. - formal/README.adoc — note that CI gates on 8.20.1 while this file documents 8.18, and that reconciling them is outstanding. STATE.a2ml was deliberately left alone: it is 67KB, self-describes as stale and as mirroring rather than leading, so a session record is the correct home. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
![gitar-bot[bot]](https://avatars.githubusercontent.com/in/827041?s=60&v=4){kind=small}
This comment was marked as resolved.
This comment was marked as resolved.
Sorry, something went wrong.
|
Note Automatic reviews are paused because your trial's included automatic processing has been used for this period. Upgrade now, or comment "Gitar review" to run a review anytime. Code Review ✅ Approved 1 resolved / 1 findingsAdds documentation for the Coq proof gate and the 2026-07-29 rescue session, but the docs describe workflow remedies that are absent from the committed gate. ✅ 1 resolved✅ Quality: Docs describe workflow remedies absent from the committed gate
OptionsDisplay: compact → Showing less information. Comment with these commands to change the behavior for this request:
Important Your trial ends in 7 days — upgrade now to keep code review, CI analysis, auto-apply, custom automations, and more. Was this helpful? React with 👍 / 👎 | Gitar |
✅ All code review findings resolved.
|
1 participant
Documentation of the state established on 2026-07-29, in both human- and
machine-readable form, using conventions already present in the repo.
docs/ci/COQ-PROOF-GATE.adocSits beside the existing
docs/ci/required-checks.adoc. Covers:Closed under the global contexttools/check-proofs.shis explicitly nota model to copy: it gates Idris2/Lean/Agda behind
command -v … || SKIPandexits
0on a machine with no provers at allformal/justfilestays the single source of truth for the proof listcoqorg/*images under GitHub Actions that will recur on any new Coq job:the overridden
ENTRYPOINT, and the silent fallback tosh/dash.machine_readable/sessions/2026-07-29-proof-gate-and-rescue.a2mlSession record on the existing
a2ml/session-record/v1schema, alongside the2026-05-27entry. Verified to parse as TOML. Records the gate, the rescue ofthree feature commits from a checkout that was deleted mid-session, three pieces
of sweep damage, the partial-merge incident that left
mainred, and methodnotes worth not re-deriving.
formal/README.adocNotes that CI gates on 8.20.1 while the file documents 8.18, that the
corpus checks clean on 8.20, and that reconciling the two is outstanding.
Not touched
STATE.a2mlwas deliberately left alone — it is 67KB, self-describes as staleand as mirroring rather than leading. A session record is the correct home for
this.
🤖 Generated with Claude Code